(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x469436ee2ce11e18) #x234a1b7716708f0c))
(constraint (= (f #x055a5d74c7b61582) #x055a5d74c7b61584))
(constraint (= (f #xcbe4ec8e7ed6ce59) #x65f276473f6b672c))
(constraint (= (f #x5e08bb3557b6182b) #x2f045d9aabdb0c15))
(constraint (= (f #x189325c875b6ae34) #x189325c875b6ae36))
(constraint (= (f #x6340dc0eb64c560e) #x6340dc0eb64c5610))
(constraint (= (f #xe946ee5e1e936127) #x0000000000000002))
(constraint (= (f #x5ec1215abb9315dd) #x0000000000000002))
(constraint (= (f #x264b51de470de8d6) #x1325a8ef2386f46b))
(constraint (= (f #x367ca7386094ae59) #x1b3e539c304a572c))
(constraint (= (f #x9b88622042792cbe) #x4dc43110213c965f))
(constraint (= (f #x36c16037dde791e8) #x1b60b01beef3c8f4))
(constraint (= (f #x15e296ca2ee0a99b) #x0af14b65177054cd))
(constraint (= (f #xada75e71e997bed4) #x56d3af38f4cbdf6a))
(constraint (= (f #x41ecc397b98b2062) #x20f661cbdcc59031))
(constraint (= (f #xe86010905abaee35) #x743008482d5d771a))
(constraint (= (f #xae3010c4922392d2) #x571808624911c969))
(constraint (= (f #x8cb83e6e19b9d9ec) #x465c1f370cdcecf6))
(constraint (= (f #x0c12b5a34240e0a1) #x06095ad1a1207050))
(constraint (= (f #x96ee54d75e7dd2c8) #x4b772a6baf3ee964))
(constraint (= (f #x8512c09dc62e46a8) #x8512c09dc62e46aa))
(constraint (= (f #xe15313aa5c17c789) #x0000000000000002))
(constraint (= (f #x39e82b1c41dd1e21) #x0000000000000002))
(constraint (= (f #x288204e1c41e681e) #x288204e1c41e6820))
(constraint (= (f #x5704a643c7ae8a09) #x2b825321e3d74504))
(constraint (= (f #x3e956b2a3192b01d) #x1f4ab59518c9580e))
(constraint (= (f #x52a46ee5dda2e910) #x52a46ee5dda2e912))
(constraint (= (f #x170c4ab970899c2a) #x0b86255cb844ce15))
(constraint (= (f #xb3dee55da19019e1) #x59ef72aed0c80cf0))
(constraint (= (f #xc6446686eb55773e) #x6322334375aabb9f))
(constraint (= (f #xb7b96506ec1e025b) #x5bdcb283760f012d))
(constraint (= (f #x59d141a08174b5ab) #x2ce8a0d040ba5ad5))
(constraint (= (f #x5b61c6ac931eece5) #x2db0e356498f7672))
(constraint (= (f #x546ee8de74b55965) #x0000000000000002))
(constraint (= (f #x99aee1ea9dd69078) #x99aee1ea9dd6907a))
(constraint (= (f #x07158e9c49532a71) #x0000000000000002))
(constraint (= (f #x8be41d61c406e151) #x45f20eb0e20370a8))
(constraint (= (f #xa35a27aed650b70c) #xa35a27aed650b70e))
(constraint (= (f #x43e825401063d153) #x0000000000000002))
(constraint (= (f #x2dd178269e1c52ee) #x2dd178269e1c52f0))
(constraint (= (f #xe9899be857c11b9a) #x74c4cdf42be08dcd))
(constraint (= (f #xbe1ea33a4b567723) #x5f0f519d25ab3b91))
(constraint (= (f #x3bc28ede547eb03b) #x1de1476f2a3f581d))
(constraint (= (f #xedce55ed59946e58) #xedce55ed59946e5a))
(constraint (= (f #x1391924035263cbe) #x1391924035263cc0))
(constraint (= (f #xcc99949052914582) #x664cca482948a2c1))
(constraint (= (f #xe9303eb7e800d71e) #xe9303eb7e800d720))
(constraint (= (f #x66b3ed2bb076dab7) #x3359f695d83b6d5b))
(constraint (= (f #xebae7c912cbee99d) #x75d73e48965f74ce))
(constraint (= (f #xc525904ae2272053) #x0000000000000002))
(constraint (= (f #xdd9a67ab4451edc3) #x0000000000000002))
(constraint (= (f #xbe9e7b422498ceee) #xbe9e7b422498cef0))
(constraint (= (f #x12c45a9718ea239e) #x12c45a9718ea23a0))
(constraint (= (f #xb6a842bd39b4eabe) #xb6a842bd39b4eac0))
(constraint (= (f #x53de4352151e7090) #x53de4352151e7092))
(constraint (= (f #xb7ad21ee2cb5239b) #x0000000000000002))
(constraint (= (f #x077517b4bd8111cb) #x0000000000000002))
(constraint (= (f #xb2ec82ade79e85b5) #x59764156f3cf42da))
(constraint (= (f #x6de12ea1292c9432) #x6de12ea1292c9434))
(constraint (= (f #x952a074edb6d25e6) #x4a9503a76db692f3))
(constraint (= (f #xb25e8e16d11d0695) #x0000000000000002))
(constraint (= (f #x4b731a4ac91462e0) #x4b731a4ac91462e2))
(constraint (= (f #xd596d7dd91b1614d) #x0000000000000002))
(constraint (= (f #x43369016e28a8ee0) #x43369016e28a8ee2))
(constraint (= (f #xb23880a217c195ac) #x591c40510be0cad6))
(constraint (= (f #x7d68b539b151e438) #x3eb45a9cd8a8f21c))
(constraint (= (f #x4cae3a3ad6a8ae05) #x26571d1d6b545702))
(constraint (= (f #xb2b597928e0a31be) #xb2b597928e0a31c0))
(constraint (= (f #xb0eb23d1ce96a464) #xb0eb23d1ce96a466))
(constraint (= (f #x119bb3b903853e2e) #x08cdd9dc81c29f17))
(constraint (= (f #x21ebe0ae6b41e337) #x0000000000000002))
(constraint (= (f #x8527333ee5053982) #x4293999f72829cc1))
(constraint (= (f #x39992e6632beeee1) #x1ccc9733195f7770))
(constraint (= (f #xb1ec7d4de8847a18) #xb1ec7d4de8847a1a))
(constraint (= (f #xa35ab36790a5e0c7) #x0000000000000002))
(constraint (= (f #x8b7ee591ec7acb46) #x8b7ee591ec7acb48))
(constraint (= (f #xe1ec3b82becc83b0) #xe1ec3b82becc83b2))
(constraint (= (f #x6472795839ac8e57) #x32393cac1cd6472b))
(constraint (= (f #xe7013831e0ec745a) #xe7013831e0ec745c))
(constraint (= (f #x4912eb4b5ea96136) #x248975a5af54b09b))
(constraint (= (f #x42984338e1d9e710) #x214c219c70ecf388))
(constraint (= (f #x3724b4deeaeb14e7) #x0000000000000002))
(constraint (= (f #x3282288e9b744e67) #x194114474dba2733))
(constraint (= (f #xbae90e50e59c0b88) #xbae90e50e59c0b8a))
(constraint (= (f #x211c5e82ac7c51cc) #x211c5e82ac7c51ce))
(constraint (= (f #x518865a37ce068d8) #x518865a37ce068da))
(constraint (= (f #x796dcb1438370747) #x0000000000000002))
(constraint (= (f #x68ba7a4be0337a9a) #x345d3d25f019bd4d))
(constraint (= (f #x5a2474e88854c7eb) #x2d123a74442a63f5))
(constraint (= (f #xdbcc68440e3e1eb3) #x6de63422071f0f59))
(constraint (= (f #x613ecb7b89047d34) #x613ecb7b89047d36))
(constraint (= (f #x0934c218844d953e) #x049a610c4226ca9f))
(constraint (= (f #x899e0eeedab47905) #x44cf07776d5a3c82))
(constraint (= (f #x0c20d3838ce72c1c) #x061069c1c673960e))
(constraint (= (f #xd3b090b97a15be55) #x0000000000000002))
(constraint (= (f #x52497712c99ed2c7) #x2924bb8964cf6963))
(constraint (= (f #x6982b6aedcd1e32d) #x0000000000000002))
(constraint (= (f #xb8db61c6e0c71760) #x5c6db0e370638bb0))
(constraint (= (f #x16c220d5584506c3) #x0000000000000002))
(constraint (= (f #x85e9548a48768c91) #x42f4aa45243b4648))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvor #x0000000000000001 x) x) (ite (= (bvurem x #x0000000000000005) #x0000000000000001) (ite (= (bvor #x000000000000000c x) x) #x0000000000000002 (bvudiv x #x0000000000000002)) (ite (= (bvand #x0000000000000009 x) #x0000000000000001) (ite (= (bvor #x0000000000000003 x) x) (ite (= (bvurem x #x0000000000000006) #x0000000000000001) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (bvudiv x #x0000000000000002) (ite (= (bvor #x0000000000000010 x) x) #x0000000000000002 (ite (= (bvurem x #x000000000000000b) #x0000000000000000) #x0000000000000002 (ite (= (bvurem x #x0000000000000007) #x0000000000000001) #x0000000000000002 (bvudiv x #x0000000000000002))))) #x0000000000000002) (ite (= (bvurem x #x000000000000000b) #x0000000000000001) #x0000000000000002 (ite (= (bvsrem x #x0000000000000003) #x0000000000000000) (bvudiv x #x0000000000000002) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvudiv x #x0000000000000002) (ite (= (bvurem x #x000000000000000d) #x0000000000000001) (bvudiv x #x0000000000000002) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (ite (= (bvor #x0000000000000010 x) x) #x0000000000000002 (bvudiv x #x0000000000000002)) #x0000000000000002)))))) (ite (= (bvurem x #x000000000000000c) #x0000000000000001) (bvudiv x #x0000000000000002) (ite (= (bvurem x #x0000000000000006) #x0000000000000001) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvudiv x #x0000000000000002) #x0000000000000002) (ite (= (bvor #x0000000000000010 x) x) (bvudiv x #x0000000000000002) (ite (= (bvor #x0000000000000003 x) x) (bvudiv x #x0000000000000002) #x0000000000000002)))))) (ite (= (bvurem x #x000000000000000c) #x0000000000000000) (ite (= (bvurem x #x000000000000000d) #x0000000000000000) (bvudiv x #x0000000000000002) (bvxor #x0000000000000002 x)) (ite (= (bvurem x #x000000000000000b) #x0000000000000000) (bvudiv x #x0000000000000002) (ite (= (bvor #x000000000000000e x) x) (ite (= (bvor #x0000000000000010 x) x) (ite (= (bvurem x #x0000000000000003) #x0000000000000001) (bvadd #x0000000000000002 x) (ite (= (bvurem x #x0000000000000006) #x0000000000000000) (ite (= (bvsrem x #x0000000000000009) #x0000000000000000) (ite (= (bvurem x #x000000000000000b) #x0000000000000001) (bvadd #x0000000000000002 x) (bvudiv x #x0000000000000002)) (bvadd #x0000000000000002 x)) (bvudiv x #x0000000000000002))) (bvadd #x0000000000000002 x)) (ite (= (bvurem x #x0000000000000007) #x0000000000000000) (bvudiv x #x0000000000000002) (ite (= (bvand #x000000000000000e x) #x0000000000000000) (bvxor #x0000000000000002 x) (ite (= (bvsrem x #x000000000000000a) #x0000000000000000) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (ite (= (bvor #x0000000000000010 x) x) (bvxor #x0000000000000002 x) (bvudiv x #x0000000000000002)) (bvudiv x #x0000000000000002)) (ite (= (bvsrem x #x0000000000000009) #x0000000000000000) (bvxor #x0000000000000002 x) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvxor #x0000000000000002 x) (ite (= (bvor #x0000000000000010 x) x) (ite (= (bvand #x000000000000000c x) #x0000000000000000) (bvxor #x0000000000000006 x) (ite (= (bvor #x000000000000000a x) x) (ite (= (bvurem x #x0000000000000006) #x0000000000000000) (bvudiv x #x0000000000000002) (bvxor #x0000000000000006 x)) (bvudiv x #x0000000000000002))) (ite (= (bvurem x #x0000000000000006) #x0000000000000000) (bvudiv x #x0000000000000002) (bvadd #x0000000000000002 x)))))))))))))
